Inference at * 1 1 1 2 1 
Iof proof for Lemma comp nat ind tp:

.....wf..... NILNIL

1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. i : 
  (i + 1)   

latex

 by ArithMemberReflEqTypeCD 

latex

 1: 

 1:   (i + 1)  
 2: .....set predicate..... NILNIL

 2:   0  (i + 1)
 3: .....wf..... NILNIL

 3: 4. i1 : 
 3:   (0  i1)  Type
 .

Definitions	t  T,
Lemmas	le wf